@InProceedings{SantosSantVija:2014:CoUMBe,
               author = "Santos, Luciana Brasil Rebelo and Santiago J{\'u}nior, Valdivino 
                         Alexandre de and Vijaykumar, Nandamudi Lankalapalli",
          affiliation = "{Instituto Nacional de Pesquisas Espaciais (INPE)} and {Instituto 
                         Nacional de Pesquisas Espaciais (INPE)}",
                title = "Converting UML behavioral diagrams to transition systems",
            booktitle = "Resumos...",
                 year = "2014",
               editor = "Santiago J{\'u}nior, Valdivino Alexandre de and Ferreira, Karine 
                         Reis",
         organization = "Workshop dos Cursos de Computa{\c{c}}{\~a}o Aplicada do INPE, 
                         14. (WORCAP).",
            publisher = "Instituto Nacional de Pesquisas Espaciais (INPE)",
              address = "S{\~a}o Jos{\'e} dos Campos",
             keywords = "UML, formal verification, model checking.",
             abstract = "ABSTRACT: This paper presents an approach related to Model-Driven 
                         Development and Formal Verification. Our approach transforms up to 
                         three different UML behavioral diagrams (sequence, activity, 
                         behavioral state machines) into a single Transition System (TS) to 
                         support Model Checking of software developed in accordance with 
                         UML. We consider properties generated from use case descriptions, 
                         which represent the requirements, and the TS translated from the 
                         behavioral diagrams. Our verification essentially consists of 
                         sequence of scenarios to be checked. Besides, the single TS has a 
                         unified view of different perspectives of behavioral modeling of 
                         the system, obtained by using various UML diagrams. In order to 
                         verify the effectiveness of our approach, we have carried out two 
                         case studies. In our experiments we have considered five different 
                         diagrams: two from ATM (Automated Teller Machine), and three from 
                         SWPDC (Software for the Payload Data Handling Computer), a real 
                         space software product, which has been developed for some 
                         scientific application projects at INPE. A tool was developed to 
                         support this approach. The main contribution of our work is the 
                         transformation of a non-formal language (UML) to a formal language 
                         (language of the NuSMV model checker) towards a greater adoption 
                         in practice of Formal Methods in software development.",
  conference-location = "S{\~a}o Jos{\'e} dos Campos",
      conference-year = "12-13 nov. 2014",
             language = "en",
         organisation = "Instituto Nacional de Pesquisas Espaciais (INPE)",
                  ibi = "8JMKD3MGP8W/3HBQ8MS",
                  url = "http://urlib.net/ibi/8JMKD3MGP8W/3HBQ8MS",
           targetfile = "worcap2014_submission_8.pdf",
        urlaccessdate = "10 maio 2024"
}